Андрей Бауэр тоже за минимальные ядра

Вот тут Андрей Байер (может быть известный программистам по Programming
Languages Zoo — сборнике имплементаций ML вариаций), в лекции посвященной
элиминатору индукции и равенству выраженному в чистой лямбде, в секции ответов
на вопросы, говорит, что критически важно иметь простое ядро прувера:

https://youtu.be/IlfQjWqrK6I?t=3690